$\forall$$T$:Type, ${\it as}$,${\it as'}$,${\it bs}$,${\it cs}$:($T$ List).
\\[0ex]($\parallel$${\it as}$$\parallel$ = $\parallel$${\it as'}$$\parallel$ $\in$ $\mathbb{Z}$) $\Rightarrow$ (append(${\it cs}$; ${\it as}$) = append(${\it bs}$; ${\it as'}$) $\in$ ($T$ List)) $\Rightarrow$ (${\it cs}$ = ${\it bs}$)